Good.

So, remember, we're in the process of designing logic-based agents.

Logic-based means we use world description languages, we call logics, to represent the world.

That is a very flexible but somewhat costly operation.

So we're only going to use it in environments where the simpler methods like CSP or so aren't promising.

So we've looked at propositional logic, which is a good world representation language,

as long as the domains we're talking about are relatively small.

What small means depends on what your technology is.

Small typically means a couple of ten thousand objects with two handfuls of properties or attributes each.

Then we can use standard techniques like DPLL solvers.

Just download Minion, hit the on button, and then you'll probably get good results.

If you have bigger domains, especially infinite domains, or possibly infinite domains, then you have to have a better logic.

That's what we're doing with first-order logic. Remember, first-order logic, the characteristics is somewhat surprising.

There's never a small chalk here.

Somebody seems to throw them away always.

The characteristics of this logic is essentially PLNQ, which gives us individuals, properties of individuals, functions of individuals.

First-order logic gives us, for example, a complete game changer if you want.

We have bound variables, they can be renamed.

We have free variables, as in say p of x, y, and those we can handle with substitutions.

Things like a for x, f of b for y.

If I apply that, I'm getting p of x becomes a, y becomes f of b, and I get this.

We need that because if we want to do something with for all x, a, I will just need something like b for x, a.

Substitutions make variables into variables if you want.

They allow you to replace the variables by arbitrary terms.

We've looked at natural deduction, which for instance has this rule called for all elimination.

There are three more rules that we can use.

That in principle gives us a way of doing inference.

Unfortunately, just as in propositional logic, and we're doing kind of the same steps as we did in propositional logic,

we don't have...

It's not easy to automate proof search with natural deduction.

It can be done, but it's not efficient.

So a much better idea would be to take something like tableau, where we have this sense of direction.

The direction into the closed branches, which kind of is the direction towards small literals,

and lift that to first of all logic.

And by and large, all propositional logic inference procedures can be lifted to the first level.

The techniques of doing that are almost always the same.

But sometimes, kind of the good systems don't survive.

So DPLL will not survive.

It will not be... You can do first order DPLL, not a problem.

It's just not going to give you good satisfiability checkers.

Other things...

get much better. Resolution gets much better.

Tableau also doesn't survive so well.

Better than DPLL, but tableau doesn't survive so well.

And before I go on, I would like to basically make a very quick survey

into first order and then even more expressive inference.

We're essentially seeing two kinds of applications of first order inference.

We're seeing something called automated theorem provers.

And automated theorem provers are things that you give a conjecture,

you press a button, you wait,